E,T,X1,X2:Type, info:(E((:Id  X1) + (:(:IdLnk  E)  X2))), e:E, f:(IdT), g:(IdLnkET).
ecase1(e;info;i.f(i);l,e'.g(l,e'))  T 

latex

Definitions	x:A. B(x), t  T, ecase1(e;info;i.f(i);l,e'.g(l;e')), x(s), x(s1,s2), t.1, t.2, P  Q
Lemmas	IdLnk wf, Id wf